Nuprl Lemma : mod_bounds
13,42
postcript
pdf
a
:
,
n
:
. (0
(
a
mod
n
)) & ((
a
mod
n
) <
n
)
latex
Up
int
2
,
int
2
Definitions
t
T
,
P
&
Q
,
x
:
A
.
B
(
x
)
,
a
mod
n
,
T
,
P
Q
,
P
Q
,
P
Q
,
True
,
ff
,
if
b
then
t
else
f
fi
,
,
tt
,
,
False
,
A
,
a
b
T
,
i
j
,
Unit
,
,
,
A
B
,
Lemmas
nat
plus
wf
,
modulus
wf
,
le
wf
,
nat
properties
,
assert
of
lt
int
,
bnot
of
le
int
,
true
wf
,
squash
wf
,
eqff
to
assert
,
assert
of
le
int
,
eqtt
to
assert
,
iff
transitivity
,
bnot
wf
,
lt
int
wf
,
assert
wf
,
bool
wf
,
le
int
wf
,
rem
bounds
1
,
not
functionality
wrt
iff
,
assert
of
bnot
,
assert
of
eq
int
,
not
wf
,
eq
int
wf
,
add
cancel
in
lt
origin